Nuprl Lemma : sum_of_geometric_prog_q
11,40
postcript
pdf
a
:
,
n
:
. ((1 + -(
a
)) *
0
i
<
n
.
a
i
) = (1 + -(
a
n
))
latex
Definitions
t
T
,
t
.2
,
t
.1
,
<
+*>
,
-
r
,
1
,
+
r
,
*
,
x
f
y
,
|
r
|
,
x
:
A
.
B
(
x
)
,
r
n
,
a
j
<
b
.
E
(
j
)
Lemmas
qrng
wf
,
sum
of
geometric
prog
origin
a:
, n:
. ((1 + -(a)) * 
0 
i < n. a 
i) = (1 + -(a n)) 
a:, n:. ((1 + -(a)) * 0 i < n. a i) = (1 + -(a n)) T+*>x:A. B(x) na j < b. E(j)